The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

0(1(2(x1))) → 0(0(2(1(x1))))
0(1(2(x1))) → 0(2(1(3(x1))))
0(1(2(x1))) → 0(0(2(1(4(4(x1))))))
0(3(1(x1))) → 0(1(3(4(0(x1)))))
0(3(1(x1))) → 0(1(3(4(4(x1)))))
0(3(1(x1))) → 1(3(4(4(4(0(x1))))))
0(3(2(x1))) → 0(2(1(3(x1))))
0(3(2(x1))) → 0(2(3(4(x1))))
0(3(2(x1))) → 0(0(2(4(3(x1)))))
0(3(2(x1))) → 0(2(1(4(3(x1)))))
0(3(2(x1))) → 0(2(4(3(3(x1)))))
0(3(2(x1))) → 0(2(1(3(3(4(x1))))))
0(3(2(x1))) → 0(2(3(4(5(5(x1))))))
0(3(2(x1))) → 2(4(4(3(4(0(x1))))))
0(4(1(x1))) → 0(1(4(4(x1))))
0(4(1(x1))) → 0(2(1(4(x1))))
0(4(2(x1))) → 0(2(1(4(x1))))
0(4(2(x1))) → 0(2(3(4(x1))))
0(4(2(x1))) → 0(2(4(3(x1))))
2(0(1(x1))) → 5(0(2(1(x1))))
2(3(1(x1))) → 1(3(5(2(x1))))
2(3(1(x1))) → 0(2(1(3(5(x1)))))
2(3(1(x1))) → 1(4(3(5(2(x1)))))
0(2(0(1(x1)))) → 5(0(0(2(1(x1)))))
0(3(1(1(x1)))) → 0(1(4(1(3(4(x1))))))
0(3(2(1(x1)))) → 0(0(3(4(2(1(x1))))))
0(3(2(2(x1)))) → 1(3(4(0(2(2(x1))))))
0(4(1(2(x1)))) → 1(4(0(2(5(x1)))))
0(4(3(2(x1)))) → 2(3(4(4(0(0(x1))))))
0(5(3(1(x1)))) → 0(1(4(3(5(4(x1))))))
0(5(3(1(x1)))) → 0(1(5(3(4(0(x1))))))
0(5(3(2(x1)))) → 0(2(4(5(3(x1)))))
0(5(3(2(x1)))) → 0(2(5(3(3(x1)))))
2(0(3(1(x1)))) → 2(0(1(3(5(2(x1))))))
2(0(4(1(x1)))) → 2(0(1(4(5(x1)))))
2(5(3(2(x1)))) → 2(5(2(3(3(x1)))))
2(5(4(2(x1)))) → 0(2(5(2(4(x1)))))
0(0(3(2(1(x1))))) → 0(0(1(3(5(2(x1))))))
0(1(0(3(2(x1))))) → 0(1(4(3(2(0(x1))))))
0(1(0(3(2(x1))))) → 2(3(1(0(0(5(x1))))))
0(3(2(5(1(x1))))) → 0(2(5(1(3(3(x1))))))
0(5(1(1(2(x1))))) → 0(2(4(1(1(5(x1))))))
0(5(1(2(2(x1))))) → 0(2(5(2(1(2(x1))))))
0(5(3(2(1(x1))))) → 0(1(3(4(2(5(x1))))))
0(5(5(3(2(x1))))) → 0(2(5(1(3(5(x1))))))
2(0(3(1(1(x1))))) → 2(1(0(1(3(4(x1))))))
2(2(0(3(1(x1))))) → 1(3(0(2(5(2(x1))))))
2(2(0(5(1(x1))))) → 2(0(2(1(5(1(x1))))))
2(5(5(4(1(x1))))) → 5(5(2(1(3(4(x1))))))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(1(2(z0))) → c(0'(0(2(1(z0)))), 0'(2(1(z0))), 2'(1(z0)))
0'(1(2(z0))) → c1(0'(2(1(3(z0)))), 2'(1(3(z0))))
0'(1(2(z0))) → c2(0'(0(2(1(4(4(z0)))))), 0'(2(1(4(4(z0))))), 2'(1(4(4(z0)))))
0'(3(1(z0))) → c3(0'(1(3(4(0(z0))))), 0'(z0))
0'(3(1(z0))) → c4(0'(1(3(4(4(z0))))))
0'(3(1(z0))) → c5(0'(z0))
0'(3(2(z0))) → c6(0'(2(1(3(z0)))), 2'(1(3(z0))))
0'(3(2(z0))) → c7(0'(2(3(4(z0)))), 2'(3(4(z0))))
0'(3(2(z0))) → c8(0'(0(2(4(3(z0))))), 0'(2(4(3(z0)))), 2'(4(3(z0))))
0'(3(2(z0))) → c9(0'(2(1(4(3(z0))))), 2'(1(4(3(z0)))))
0'(3(2(z0))) → c10(0'(2(4(3(3(z0))))), 2'(4(3(3(z0)))))
0'(3(2(z0))) → c11(0'(2(1(3(3(4(z0)))))), 2'(1(3(3(4(z0))))))
0'(3(2(z0))) → c12(0'(2(3(4(5(5(z0)))))), 2'(3(4(5(5(z0))))))
0'(3(2(z0))) → c13(2'(4(4(3(4(0(z0)))))), 0'(z0))
0'(4(1(z0))) → c14(0'(1(4(4(z0)))))
0'(4(1(z0))) → c15(0'(2(1(4(z0)))), 2'(1(4(z0))))
0'(4(2(z0))) → c16(0'(2(1(4(z0)))), 2'(1(4(z0))))
0'(4(2(z0))) → c17(0'(2(3(4(z0)))), 2'(3(4(z0))))
0'(4(2(z0))) → c18(0'(2(4(3(z0)))), 2'(4(3(z0))))
0'(2(0(1(z0)))) → c19(0'(0(2(1(z0)))), 0'(2(1(z0))), 2'(1(z0)))
0'(3(1(1(z0)))) → c20(0'(1(4(1(3(4(z0)))))))
0'(3(2(1(z0)))) → c21(0'(0(3(4(2(1(z0)))))), 0'(3(4(2(1(z0))))), 2'(1(z0)))
0'(3(2(2(z0)))) → c22(0'(2(2(z0))), 2'(2(z0)), 2'(z0))
0'(4(1(2(z0)))) → c23(0'(2(5(z0))), 2'(5(z0)))
0'(4(3(2(z0)))) → c24(2'(3(4(4(0(0(z0)))))), 0'(0(z0)), 0'(z0))
0'(5(3(1(z0)))) → c25(0'(1(4(3(5(4(z0)))))))
0'(5(3(1(z0)))) → c26(0'(1(5(3(4(0(z0)))))), 0'(z0))
0'(5(3(2(z0)))) → c27(0'(2(4(5(3(z0))))), 2'(4(5(3(z0)))))
0'(5(3(2(z0)))) → c28(0'(2(5(3(3(z0))))), 2'(5(3(3(z0)))))
0'(0(3(2(1(z0))))) → c29(0'(0(1(3(5(2(z0)))))), 0'(1(3(5(2(z0))))), 2'(z0))
0'(1(0(3(2(z0))))) → c30(0'(1(4(3(2(0(z0)))))), 2'(0(z0)), 0'(z0))
0'(1(0(3(2(z0))))) → c31(2'(3(1(0(0(5(z0)))))), 0'(0(5(z0))), 0'(5(z0)))
0'(3(2(5(1(z0))))) → c32(0'(2(5(1(3(3(z0)))))), 2'(5(1(3(3(z0))))))
0'(5(1(1(2(z0))))) → c33(0'(2(4(1(1(5(z0)))))), 2'(4(1(1(5(z0))))))
0'(5(1(2(2(z0))))) → c34(0'(2(5(2(1(2(z0)))))), 2'(5(2(1(2(z0))))), 2'(1(2(z0))), 2'(z0))
0'(5(3(2(1(z0))))) → c35(0'(1(3(4(2(5(z0)))))), 2'(5(z0)))
0'(5(5(3(2(z0))))) → c36(0'(2(5(1(3(5(z0)))))), 2'(5(1(3(5(z0))))))
2'(0(1(z0))) → c37(0'(2(1(z0))), 2'(1(z0)))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c39(0'(2(1(3(5(z0))))), 2'(1(3(5(z0)))))
2'(3(1(z0))) → c40(2'(z0))
2'(0(3(1(z0)))) → c41(2'(0(1(3(5(2(z0)))))), 0'(1(3(5(2(z0))))), 2'(z0))
2'(0(4(1(z0)))) → c42(2'(0(1(4(5(z0))))), 0'(1(4(5(z0)))))
2'(5(3(2(z0)))) → c43(2'(5(2(3(3(z0))))), 2'(3(3(z0))))
2'(5(4(2(z0)))) → c44(0'(2(5(2(4(z0))))), 2'(5(2(4(z0)))), 2'(4(z0)))
2'(0(3(1(1(z0))))) → c45(2'(1(0(1(3(4(z0)))))), 0'(1(3(4(z0)))))
2'(2(0(3(1(z0))))) → c46(0'(2(5(2(z0)))), 2'(5(2(z0))), 2'(z0))
2'(2(0(5(1(z0))))) → c47(2'(0(2(1(5(1(z0)))))), 0'(2(1(5(1(z0))))), 2'(1(5(1(z0)))))
2'(5(5(4(1(z0))))) → c48(2'(1(3(4(z0)))))

S tuples:

0'(1(2(z0))) → c(0'(0(2(1(z0)))), 0'(2(1(z0))), 2'(1(z0)))
0'(1(2(z0))) → c1(0'(2(1(3(z0)))), 2'(1(3(z0))))
0'(1(2(z0))) → c2(0'(0(2(1(4(4(z0)))))), 0'(2(1(4(4(z0))))), 2'(1(4(4(z0)))))
0'(3(1(z0))) → c3(0'(1(3(4(0(z0))))), 0'(z0))
0'(3(1(z0))) → c4(0'(1(3(4(4(z0))))))
0'(3(1(z0))) → c5(0'(z0))
0'(3(2(z0))) → c6(0'(2(1(3(z0)))), 2'(1(3(z0))))
0'(3(2(z0))) → c7(0'(2(3(4(z0)))), 2'(3(4(z0))))
0'(3(2(z0))) → c8(0'(0(2(4(3(z0))))), 0'(2(4(3(z0)))), 2'(4(3(z0))))
0'(3(2(z0))) → c9(0'(2(1(4(3(z0))))), 2'(1(4(3(z0)))))
0'(3(2(z0))) → c10(0'(2(4(3(3(z0))))), 2'(4(3(3(z0)))))
0'(3(2(z0))) → c11(0'(2(1(3(3(4(z0)))))), 2'(1(3(3(4(z0))))))
0'(3(2(z0))) → c12(0'(2(3(4(5(5(z0)))))), 2'(3(4(5(5(z0))))))
0'(3(2(z0))) → c13(2'(4(4(3(4(0(z0)))))), 0'(z0))
0'(4(1(z0))) → c14(0'(1(4(4(z0)))))
0'(4(1(z0))) → c15(0'(2(1(4(z0)))), 2'(1(4(z0))))
0'(4(2(z0))) → c16(0'(2(1(4(z0)))), 2'(1(4(z0))))
0'(4(2(z0))) → c17(0'(2(3(4(z0)))), 2'(3(4(z0))))
0'(4(2(z0))) → c18(0'(2(4(3(z0)))), 2'(4(3(z0))))
0'(2(0(1(z0)))) → c19(0'(0(2(1(z0)))), 0'(2(1(z0))), 2'(1(z0)))
0'(3(1(1(z0)))) → c20(0'(1(4(1(3(4(z0)))))))
0'(3(2(1(z0)))) → c21(0'(0(3(4(2(1(z0)))))), 0'(3(4(2(1(z0))))), 2'(1(z0)))
0'(3(2(2(z0)))) → c22(0'(2(2(z0))), 2'(2(z0)), 2'(z0))
0'(4(1(2(z0)))) → c23(0'(2(5(z0))), 2'(5(z0)))
0'(4(3(2(z0)))) → c24(2'(3(4(4(0(0(z0)))))), 0'(0(z0)), 0'(z0))
0'(5(3(1(z0)))) → c25(0'(1(4(3(5(4(z0)))))))
0'(5(3(1(z0)))) → c26(0'(1(5(3(4(0(z0)))))), 0'(z0))
0'(5(3(2(z0)))) → c27(0'(2(4(5(3(z0))))), 2'(4(5(3(z0)))))
0'(5(3(2(z0)))) → c28(0'(2(5(3(3(z0))))), 2'(5(3(3(z0)))))
0'(0(3(2(1(z0))))) → c29(0'(0(1(3(5(2(z0)))))), 0'(1(3(5(2(z0))))), 2'(z0))
0'(1(0(3(2(z0))))) → c30(0'(1(4(3(2(0(z0)))))), 2'(0(z0)), 0'(z0))
0'(1(0(3(2(z0))))) → c31(2'(3(1(0(0(5(z0)))))), 0'(0(5(z0))), 0'(5(z0)))
0'(3(2(5(1(z0))))) → c32(0'(2(5(1(3(3(z0)))))), 2'(5(1(3(3(z0))))))
0'(5(1(1(2(z0))))) → c33(0'(2(4(1(1(5(z0)))))), 2'(4(1(1(5(z0))))))
0'(5(1(2(2(z0))))) → c34(0'(2(5(2(1(2(z0)))))), 2'(5(2(1(2(z0))))), 2'(1(2(z0))), 2'(z0))
0'(5(3(2(1(z0))))) → c35(0'(1(3(4(2(5(z0)))))), 2'(5(z0)))
0'(5(5(3(2(z0))))) → c36(0'(2(5(1(3(5(z0)))))), 2'(5(1(3(5(z0))))))
2'(0(1(z0))) → c37(0'(2(1(z0))), 2'(1(z0)))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c39(0'(2(1(3(5(z0))))), 2'(1(3(5(z0)))))
2'(3(1(z0))) → c40(2'(z0))
2'(0(3(1(z0)))) → c41(2'(0(1(3(5(2(z0)))))), 0'(1(3(5(2(z0))))), 2'(z0))
2'(0(4(1(z0)))) → c42(2'(0(1(4(5(z0))))), 0'(1(4(5(z0)))))
2'(5(3(2(z0)))) → c43(2'(5(2(3(3(z0))))), 2'(3(3(z0))))
2'(5(4(2(z0)))) → c44(0'(2(5(2(4(z0))))), 2'(5(2(4(z0)))), 2'(4(z0)))
2'(0(3(1(1(z0))))) → c45(2'(1(0(1(3(4(z0)))))), 0'(1(3(4(z0)))))
2'(2(0(3(1(z0))))) → c46(0'(2(5(2(z0)))), 2'(5(2(z0))), 2'(z0))
2'(2(0(5(1(z0))))) → c47(2'(0(2(1(5(1(z0)))))), 0'(2(1(5(1(z0))))), 2'(1(5(1(z0)))))
2'(5(5(4(1(z0))))) → c48(2'(1(3(4(z0)))))

K tuples:none
Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

0'(2(0(1(z0)))) → c19(0'(0(2(1(z0)))), 0'(2(1(z0))), 2'(1(z0)))
0'(0(3(2(1(z0))))) → c29(0'(0(1(3(5(2(z0)))))), 0'(1(3(5(2(z0))))), 2'(z0))
0'(1(0(3(2(z0))))) → c30(0'(1(4(3(2(0(z0)))))), 2'(0(z0)), 0'(z0))
0'(1(0(3(2(z0))))) → c31(2'(3(1(0(0(5(z0)))))), 0'(0(5(z0))), 0'(5(z0)))
2'(0(3(1(z0)))) → c41(2'(0(1(3(5(2(z0)))))), 0'(1(3(5(2(z0))))), 2'(z0))
2'(0(4(1(z0)))) → c42(2'(0(1(4(5(z0))))), 0'(1(4(5(z0)))))
2'(0(3(1(1(z0))))) → c45(2'(1(0(1(3(4(z0)))))), 0'(1(3(4(z0)))))
2'(2(0(3(1(z0))))) → c46(0'(2(5(2(z0)))), 2'(5(2(z0))), 2'(z0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c3(0'(1(3(4(0(z0))))), 0'(z0))
0'(3(1(z0))) → c4(0'(1(3(4(4(z0))))))
0'(3(1(z0))) → c5(0'(z0))
0'(4(1(z0))) → c14(0'(1(4(4(z0)))))
0'(4(1(z0))) → c15(0'(2(1(4(z0)))), 2'(1(4(z0))))
0'(3(1(1(z0)))) → c20(0'(1(4(1(3(4(z0)))))))
0'(5(3(1(z0)))) → c25(0'(1(4(3(5(4(z0)))))))
0'(5(3(1(z0)))) → c26(0'(1(5(3(4(0(z0)))))), 0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c39(0'(2(1(3(5(z0))))), 2'(1(3(5(z0)))))
2'(3(1(z0))) → c40(2'(z0))
2'(5(5(4(1(z0))))) → c48(2'(1(3(4(z0)))))
2'(0(1(z0))) → c37(0'(2(1(z0))), 2'(1(z0)))
2'(5(3(2(z0)))) → c43(2'(5(2(3(3(z0))))), 2'(3(3(z0))))
2'(5(4(2(z0)))) → c44(0'(2(5(2(4(z0))))), 2'(5(2(4(z0)))), 2'(4(z0)))
2'(2(0(5(1(z0))))) → c47(2'(0(2(1(5(1(z0)))))), 0'(2(1(5(1(z0))))), 2'(1(5(1(z0)))))
0'(1(2(z0))) → c(0'(0(2(1(z0)))), 0'(2(1(z0))), 2'(1(z0)))
0'(1(2(z0))) → c1(0'(2(1(3(z0)))), 2'(1(3(z0))))
0'(1(2(z0))) → c2(0'(0(2(1(4(4(z0)))))), 0'(2(1(4(4(z0))))), 2'(1(4(4(z0)))))
0'(3(2(z0))) → c6(0'(2(1(3(z0)))), 2'(1(3(z0))))
0'(3(2(z0))) → c7(0'(2(3(4(z0)))), 2'(3(4(z0))))
0'(3(2(z0))) → c8(0'(0(2(4(3(z0))))), 0'(2(4(3(z0)))), 2'(4(3(z0))))
0'(3(2(z0))) → c9(0'(2(1(4(3(z0))))), 2'(1(4(3(z0)))))
0'(3(2(z0))) → c10(0'(2(4(3(3(z0))))), 2'(4(3(3(z0)))))
0'(3(2(z0))) → c11(0'(2(1(3(3(4(z0)))))), 2'(1(3(3(4(z0))))))
0'(3(2(z0))) → c12(0'(2(3(4(5(5(z0)))))), 2'(3(4(5(5(z0))))))
0'(3(2(z0))) → c13(2'(4(4(3(4(0(z0)))))), 0'(z0))
0'(4(2(z0))) → c16(0'(2(1(4(z0)))), 2'(1(4(z0))))
0'(4(2(z0))) → c17(0'(2(3(4(z0)))), 2'(3(4(z0))))
0'(4(2(z0))) → c18(0'(2(4(3(z0)))), 2'(4(3(z0))))
0'(3(2(1(z0)))) → c21(0'(0(3(4(2(1(z0)))))), 0'(3(4(2(1(z0))))), 2'(1(z0)))
0'(3(2(2(z0)))) → c22(0'(2(2(z0))), 2'(2(z0)), 2'(z0))
0'(4(1(2(z0)))) → c23(0'(2(5(z0))), 2'(5(z0)))
0'(4(3(2(z0)))) → c24(2'(3(4(4(0(0(z0)))))), 0'(0(z0)), 0'(z0))
0'(5(3(2(z0)))) → c27(0'(2(4(5(3(z0))))), 2'(4(5(3(z0)))))
0'(5(3(2(z0)))) → c28(0'(2(5(3(3(z0))))), 2'(5(3(3(z0)))))
0'(3(2(5(1(z0))))) → c32(0'(2(5(1(3(3(z0)))))), 2'(5(1(3(3(z0))))))
0'(5(1(1(2(z0))))) → c33(0'(2(4(1(1(5(z0)))))), 2'(4(1(1(5(z0))))))
0'(5(1(2(2(z0))))) → c34(0'(2(5(2(1(2(z0)))))), 2'(5(2(1(2(z0))))), 2'(1(2(z0))), 2'(z0))
0'(5(3(2(1(z0))))) → c35(0'(1(3(4(2(5(z0)))))), 2'(5(z0)))
0'(5(5(3(2(z0))))) → c36(0'(2(5(1(3(5(z0)))))), 2'(5(1(3(5(z0))))))

S tuples:

0'(1(2(z0))) → c(0'(0(2(1(z0)))), 0'(2(1(z0))), 2'(1(z0)))
0'(1(2(z0))) → c1(0'(2(1(3(z0)))), 2'(1(3(z0))))
0'(1(2(z0))) → c2(0'(0(2(1(4(4(z0)))))), 0'(2(1(4(4(z0))))), 2'(1(4(4(z0)))))
0'(3(1(z0))) → c3(0'(1(3(4(0(z0))))), 0'(z0))
0'(3(1(z0))) → c4(0'(1(3(4(4(z0))))))
0'(3(1(z0))) → c5(0'(z0))
0'(3(2(z0))) → c6(0'(2(1(3(z0)))), 2'(1(3(z0))))
0'(3(2(z0))) → c7(0'(2(3(4(z0)))), 2'(3(4(z0))))
0'(3(2(z0))) → c8(0'(0(2(4(3(z0))))), 0'(2(4(3(z0)))), 2'(4(3(z0))))
0'(3(2(z0))) → c9(0'(2(1(4(3(z0))))), 2'(1(4(3(z0)))))
0'(3(2(z0))) → c10(0'(2(4(3(3(z0))))), 2'(4(3(3(z0)))))
0'(3(2(z0))) → c11(0'(2(1(3(3(4(z0)))))), 2'(1(3(3(4(z0))))))
0'(3(2(z0))) → c12(0'(2(3(4(5(5(z0)))))), 2'(3(4(5(5(z0))))))
0'(3(2(z0))) → c13(2'(4(4(3(4(0(z0)))))), 0'(z0))
0'(4(1(z0))) → c14(0'(1(4(4(z0)))))
0'(4(1(z0))) → c15(0'(2(1(4(z0)))), 2'(1(4(z0))))
0'(4(2(z0))) → c16(0'(2(1(4(z0)))), 2'(1(4(z0))))
0'(4(2(z0))) → c17(0'(2(3(4(z0)))), 2'(3(4(z0))))
0'(4(2(z0))) → c18(0'(2(4(3(z0)))), 2'(4(3(z0))))
0'(3(1(1(z0)))) → c20(0'(1(4(1(3(4(z0)))))))
0'(3(2(1(z0)))) → c21(0'(0(3(4(2(1(z0)))))), 0'(3(4(2(1(z0))))), 2'(1(z0)))
0'(3(2(2(z0)))) → c22(0'(2(2(z0))), 2'(2(z0)), 2'(z0))
0'(4(1(2(z0)))) → c23(0'(2(5(z0))), 2'(5(z0)))
0'(4(3(2(z0)))) → c24(2'(3(4(4(0(0(z0)))))), 0'(0(z0)), 0'(z0))
0'(5(3(1(z0)))) → c25(0'(1(4(3(5(4(z0)))))))
0'(5(3(1(z0)))) → c26(0'(1(5(3(4(0(z0)))))), 0'(z0))
0'(5(3(2(z0)))) → c27(0'(2(4(5(3(z0))))), 2'(4(5(3(z0)))))
0'(5(3(2(z0)))) → c28(0'(2(5(3(3(z0))))), 2'(5(3(3(z0)))))
0'(3(2(5(1(z0))))) → c32(0'(2(5(1(3(3(z0)))))), 2'(5(1(3(3(z0))))))
0'(5(1(1(2(z0))))) → c33(0'(2(4(1(1(5(z0)))))), 2'(4(1(1(5(z0))))))
0'(5(1(2(2(z0))))) → c34(0'(2(5(2(1(2(z0)))))), 2'(5(2(1(2(z0))))), 2'(1(2(z0))), 2'(z0))
0'(5(3(2(1(z0))))) → c35(0'(1(3(4(2(5(z0)))))), 2'(5(z0)))
0'(5(5(3(2(z0))))) → c36(0'(2(5(1(3(5(z0)))))), 2'(5(1(3(5(z0))))))
2'(0(1(z0))) → c37(0'(2(1(z0))), 2'(1(z0)))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c39(0'(2(1(3(5(z0))))), 2'(1(3(5(z0)))))
2'(3(1(z0))) → c40(2'(z0))
2'(5(3(2(z0)))) → c43(2'(5(2(3(3(z0))))), 2'(3(3(z0))))
2'(5(4(2(z0)))) → c44(0'(2(5(2(4(z0))))), 2'(5(2(4(z0)))), 2'(4(z0)))
2'(2(0(5(1(z0))))) → c47(2'(0(2(1(5(1(z0)))))), 0'(2(1(5(1(z0))))), 2'(1(5(1(z0)))))
2'(5(5(4(1(z0))))) → c48(2'(1(3(4(z0)))))

K tuples:none
Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c3, c4, c5, c14, c15, c20, c25, c26, c38, c39, c40, c48, c37, c43, c44, c47, c, c1, c2, c6, c7, c8, c9, c10, c11, c12, c13, c16, c17, c18, c21, c22, c23, c24, c27, c28, c32, c33, c34, c35, c36

(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 31 of 41 dangling nodes:

0'(1(2(z0))) → c(0'(0(2(1(z0)))), 0'(2(1(z0))), 2'(1(z0)))
0'(1(2(z0))) → c1(0'(2(1(3(z0)))), 2'(1(3(z0))))
0'(1(2(z0))) → c2(0'(0(2(1(4(4(z0)))))), 0'(2(1(4(4(z0))))), 2'(1(4(4(z0)))))
0'(3(1(z0))) → c4(0'(1(3(4(4(z0))))))
0'(3(2(z0))) → c6(0'(2(1(3(z0)))), 2'(1(3(z0))))
0'(3(2(z0))) → c7(0'(2(3(4(z0)))), 2'(3(4(z0))))
0'(3(2(z0))) → c8(0'(0(2(4(3(z0))))), 0'(2(4(3(z0)))), 2'(4(3(z0))))
0'(3(2(z0))) → c9(0'(2(1(4(3(z0))))), 2'(1(4(3(z0)))))
0'(3(2(z0))) → c10(0'(2(4(3(3(z0))))), 2'(4(3(3(z0)))))
0'(3(2(z0))) → c11(0'(2(1(3(3(4(z0)))))), 2'(1(3(3(4(z0))))))
0'(3(2(z0))) → c12(0'(2(3(4(5(5(z0)))))), 2'(3(4(5(5(z0))))))
0'(4(1(z0))) → c14(0'(1(4(4(z0)))))
0'(4(2(z0))) → c16(0'(2(1(4(z0)))), 2'(1(4(z0))))
0'(4(1(z0))) → c15(0'(2(1(4(z0)))), 2'(1(4(z0))))
0'(4(2(z0))) → c18(0'(2(4(3(z0)))), 2'(4(3(z0))))
0'(4(2(z0))) → c17(0'(2(3(4(z0)))), 2'(3(4(z0))))
0'(3(1(1(z0)))) → c20(0'(1(4(1(3(4(z0)))))))
0'(3(2(1(z0)))) → c21(0'(0(3(4(2(1(z0)))))), 0'(3(4(2(1(z0))))), 2'(1(z0)))
0'(5(3(1(z0)))) → c25(0'(1(4(3(5(4(z0)))))))
0'(5(3(2(z0)))) → c28(0'(2(5(3(3(z0))))), 2'(5(3(3(z0)))))
0'(5(3(2(z0)))) → c27(0'(2(4(5(3(z0))))), 2'(4(5(3(z0)))))
0'(5(1(1(2(z0))))) → c33(0'(2(4(1(1(5(z0)))))), 2'(4(1(1(5(z0))))))
0'(3(2(5(1(z0))))) → c32(0'(2(5(1(3(3(z0)))))), 2'(5(1(3(3(z0))))))
2'(0(1(z0))) → c37(0'(2(1(z0))), 2'(1(z0)))
0'(5(3(2(1(z0))))) → c35(0'(1(3(4(2(5(z0)))))), 2'(5(z0)))
0'(5(5(3(2(z0))))) → c36(0'(2(5(1(3(5(z0)))))), 2'(5(1(3(5(z0))))))
2'(3(1(z0))) → c39(0'(2(1(3(5(z0))))), 2'(1(3(5(z0)))))
2'(5(3(2(z0)))) → c43(2'(5(2(3(3(z0))))), 2'(3(3(z0))))
2'(5(4(2(z0)))) → c44(0'(2(5(2(4(z0))))), 2'(5(2(4(z0)))), 2'(4(z0)))
2'(5(5(4(1(z0))))) → c48(2'(1(3(4(z0)))))
2'(2(0(5(1(z0))))) → c47(2'(0(2(1(5(1(z0)))))), 0'(2(1(5(1(z0))))), 2'(1(5(1(z0)))))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c3(0'(1(3(4(0(z0))))), 0'(z0))
0'(3(1(z0))) → c5(0'(z0))
0'(5(3(1(z0)))) → c26(0'(1(5(3(4(0(z0)))))), 0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(z0))) → c13(2'(4(4(3(4(0(z0)))))), 0'(z0))
0'(3(2(2(z0)))) → c22(0'(2(2(z0))), 2'(2(z0)), 2'(z0))
0'(4(1(2(z0)))) → c23(0'(2(5(z0))), 2'(5(z0)))
0'(4(3(2(z0)))) → c24(2'(3(4(4(0(0(z0)))))), 0'(0(z0)), 0'(z0))
0'(5(1(2(2(z0))))) → c34(0'(2(5(2(1(2(z0)))))), 2'(5(2(1(2(z0))))), 2'(1(2(z0))), 2'(z0))

S tuples:

0'(3(1(z0))) → c3(0'(1(3(4(0(z0))))), 0'(z0))
0'(3(1(z0))) → c5(0'(z0))
0'(3(2(z0))) → c13(2'(4(4(3(4(0(z0)))))), 0'(z0))
0'(3(2(2(z0)))) → c22(0'(2(2(z0))), 2'(2(z0)), 2'(z0))
0'(4(1(2(z0)))) → c23(0'(2(5(z0))), 2'(5(z0)))
0'(4(3(2(z0)))) → c24(2'(3(4(4(0(0(z0)))))), 0'(0(z0)), 0'(z0))
0'(5(3(1(z0)))) → c26(0'(1(5(3(4(0(z0)))))), 0'(z0))
0'(5(1(2(2(z0))))) → c34(0'(2(5(2(1(2(z0)))))), 2'(5(2(1(2(z0))))), 2'(1(2(z0))), 2'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))

K tuples:none
Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c3, c5, c26, c38, c40, c13, c22, c23, c24, c34

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c3(0'(1(3(4(0(z0))))), 0'(z0))
0'(3(1(z0))) → c5(0'(z0))
0'(5(3(1(z0)))) → c26(0'(1(5(3(4(0(z0)))))), 0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(z0))) → c13(2'(4(4(3(4(0(z0)))))), 0'(z0))
0'(4(1(2(z0)))) → c23(0'(2(5(z0))), 2'(5(z0)))
0'(4(3(2(z0)))) → c24(2'(3(4(4(0(0(z0)))))), 0'(0(z0)), 0'(z0))
0'(3(2(2(z0)))) → c(0'(2(2(z0))))
0'(3(2(2(z0)))) → c(2'(2(z0)))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(0'(2(5(2(1(2(z0)))))))
0'(5(1(2(2(z0))))) → c(2'(5(2(1(2(z0))))))
0'(5(1(2(2(z0))))) → c(2'(1(2(z0))))
0'(5(1(2(2(z0))))) → c(2'(z0))

S tuples:

0'(3(1(z0))) → c3(0'(1(3(4(0(z0))))), 0'(z0))
0'(3(1(z0))) → c5(0'(z0))
0'(3(2(z0))) → c13(2'(4(4(3(4(0(z0)))))), 0'(z0))
0'(4(1(2(z0)))) → c23(0'(2(5(z0))), 2'(5(z0)))
0'(4(3(2(z0)))) → c24(2'(3(4(4(0(0(z0)))))), 0'(0(z0)), 0'(z0))
0'(5(3(1(z0)))) → c26(0'(1(5(3(4(0(z0)))))), 0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(0'(2(2(z0))))
0'(3(2(2(z0)))) → c(2'(2(z0)))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(0'(2(5(2(1(2(z0)))))))
0'(5(1(2(2(z0))))) → c(2'(5(2(1(2(z0))))))
0'(5(1(2(2(z0))))) → c(2'(1(2(z0))))
0'(5(1(2(2(z0))))) → c(2'(z0))

K tuples:none
Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c3, c5, c26, c38, c40, c13, c23, c24, c

(9) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 10 trailing tuple parts

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(1(2(z0)))) → c23(0'(2(5(z0))))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))
0'(3(2(2(z0)))) → c
0'(5(1(2(2(z0))))) → c

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(1(2(z0)))) → c23(0'(2(5(z0))))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))
0'(3(2(2(z0)))) → c
0'(5(1(2(2(z0))))) → c

K tuples:none
Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c, c3, c26, c13, c23, c24, c

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace 0'(4(1(2(z0)))) → c23(0'(2(5(z0)))) by

0'(4(1(2(3(2(z0)))))) → c23(0'(2(5(2(3(3(z0)))))))
0'(4(1(2(4(2(z0)))))) → c23(0'(0(2(5(2(4(z0)))))))
0'(4(1(2(5(4(1(z0))))))) → c23(0'(5(5(2(1(3(4(z0))))))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))
0'(3(2(2(z0)))) → c
0'(5(1(2(2(z0))))) → c
0'(4(1(2(3(2(z0)))))) → c23(0'(2(5(2(3(3(z0)))))))
0'(4(1(2(4(2(z0)))))) → c23(0'(0(2(5(2(4(z0)))))))
0'(4(1(2(5(4(1(z0))))))) → c23(0'(5(5(2(1(3(4(z0))))))))

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))
0'(3(2(2(z0)))) → c
0'(5(1(2(2(z0))))) → c
0'(4(1(2(3(2(z0)))))) → c23(0'(2(5(2(3(3(z0)))))))
0'(4(1(2(4(2(z0)))))) → c23(0'(0(2(5(2(4(z0)))))))
0'(4(1(2(5(4(1(z0))))))) → c23(0'(5(5(2(1(3(4(z0))))))))

K tuples:none
Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c, c3, c26, c13, c24, c, c23

(13) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 5 of 14 dangling nodes:

0'(5(1(2(2(z0))))) → c
0'(3(2(2(z0)))) → c
0'(4(1(2(4(2(z0)))))) → c23(0'(0(2(5(2(4(z0)))))))
0'(4(1(2(5(4(1(z0))))))) → c23(0'(5(5(2(1(3(4(z0))))))))
0'(4(1(2(3(2(z0)))))) → c23(0'(2(5(2(3(3(z0)))))))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))

K tuples:none
Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c, c3, c26, c13, c24

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(5(3(1(z0)))) → c26(0'(z0))

We considered the (Usable) Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0   
POL(0'(x₁)) = [4]x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = [4]x₁   
POL(2'(x₁)) = 0   
POL(3(x₁)) = x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = [1] + x₁   
POL(c(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁, x₂)) = x₁ + x₂   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c, c3, c26, c13, c24

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(5(1(2(2(z0))))) → c(2'(z0))

We considered the (Usable) Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0   
POL(0'(x₁)) = x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = [2]x₁   
POL(2'(x₁)) = 0   
POL(3(x₁)) = x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = [4] + x₁   
POL(c(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁, x₂)) = x₁ + x₂   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c, c3, c26, c13, c24

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace 0'(4(3(2(z0)))) → c24(0'(0(z0)), 0'(z0)) by

0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(z0))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(4(4(z0))))))), 0'(1(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(0(2(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(4(3(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(3(4(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(5(5(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(2(4(4(3(4(0(z0))))))), 0'(3(2(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(1(4(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(4(3(z0))))), 0'(4(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(0(0(3(4(2(1(z0))))))), 0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(1(3(4(0(2(2(z0))))))), 0'(3(2(2(z0)))))
0'(4(3(2(4(1(2(z0))))))) → c24(0'(1(4(0(2(5(z0)))))), 0'(4(1(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(2(3(4(4(0(0(z0))))))), 0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(4(3(5(4(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(5(3(4(0(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(0(2(5(1(3(3(z0))))))), 0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(1(2(z0)))))))) → c24(0'(0(2(4(1(1(5(z0))))))), 0'(5(1(1(2(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c24(0'(0(2(5(2(1(2(z0))))))), 0'(5(1(2(2(z0))))))
0'(4(3(2(5(5(3(2(z0)))))))) → c24(0'(0(2(5(1(3(5(z0))))))), 0'(5(5(3(2(z0))))))
0'(4(3(2(3(1(z0)))))) → c24(0'(0(1(3(4(0(z0)))))), 0'(3(1(z0))))
0'(4(3(2(3(1(z0)))))) → c24(0'(0(1(3(4(4(z0)))))), 0'(3(1(z0))))
0'(4(3(2(3(1(z0)))))) → c24(0'(1(3(4(4(4(0(z0))))))), 0'(3(1(z0))))
0'(4(3(2(3(1(1(z0))))))) → c24(0'(0(1(4(1(3(4(z0))))))), 0'(3(1(1(z0)))))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(z0))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(4(4(z0))))))), 0'(1(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(0(2(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(4(3(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(3(4(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(5(5(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(2(4(4(3(4(0(z0))))))), 0'(3(2(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(1(4(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(4(3(z0))))), 0'(4(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(0(0(3(4(2(1(z0))))))), 0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(1(3(4(0(2(2(z0))))))), 0'(3(2(2(z0)))))
0'(4(3(2(4(1(2(z0))))))) → c24(0'(1(4(0(2(5(z0)))))), 0'(4(1(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(2(3(4(4(0(0(z0))))))), 0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(4(3(5(4(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(5(3(4(0(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(0(2(5(1(3(3(z0))))))), 0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(1(2(z0)))))))) → c24(0'(0(2(4(1(1(5(z0))))))), 0'(5(1(1(2(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c24(0'(0(2(5(2(1(2(z0))))))), 0'(5(1(2(2(z0))))))
0'(4(3(2(5(5(3(2(z0)))))))) → c24(0'(0(2(5(1(3(5(z0))))))), 0'(5(5(3(2(z0))))))
0'(4(3(2(3(1(z0)))))) → c24(0'(0(1(3(4(0(z0)))))), 0'(3(1(z0))))
0'(4(3(2(3(1(z0)))))) → c24(0'(0(1(3(4(4(z0)))))), 0'(3(1(z0))))
0'(4(3(2(3(1(z0)))))) → c24(0'(1(3(4(4(4(0(z0))))))), 0'(3(1(z0))))
0'(4(3(2(3(1(1(z0))))))) → c24(0'(0(1(4(1(3(4(z0))))))), 0'(3(1(1(z0)))))

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(z0))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(4(4(z0))))))), 0'(1(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(0(2(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(4(3(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(3(4(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(5(5(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(2(4(4(3(4(0(z0))))))), 0'(3(2(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(1(4(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(4(3(z0))))), 0'(4(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(0(0(3(4(2(1(z0))))))), 0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(1(3(4(0(2(2(z0))))))), 0'(3(2(2(z0)))))
0'(4(3(2(4(1(2(z0))))))) → c24(0'(1(4(0(2(5(z0)))))), 0'(4(1(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(2(3(4(4(0(0(z0))))))), 0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(4(3(5(4(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(5(3(4(0(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(0(2(5(1(3(3(z0))))))), 0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(1(2(z0)))))))) → c24(0'(0(2(4(1(1(5(z0))))))), 0'(5(1(1(2(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c24(0'(0(2(5(2(1(2(z0))))))), 0'(5(1(2(2(z0))))))
0'(4(3(2(5(5(3(2(z0)))))))) → c24(0'(0(2(5(1(3(5(z0))))))), 0'(5(5(3(2(z0))))))
0'(4(3(2(3(1(z0)))))) → c24(0'(0(1(3(4(0(z0)))))), 0'(3(1(z0))))
0'(4(3(2(3(1(z0)))))) → c24(0'(0(1(3(4(4(z0)))))), 0'(3(1(z0))))
0'(4(3(2(3(1(z0)))))) → c24(0'(1(3(4(4(4(0(z0))))))), 0'(3(1(z0))))
0'(4(3(2(3(1(1(z0))))))) → c24(0'(0(1(4(1(3(4(z0))))))), 0'(3(1(1(z0)))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c, c3, c26, c13, c24

(21) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

0'(4(3(2(3(1(z0)))))) → c24(0'(0(1(3(4(0(z0)))))), 0'(3(1(z0))))
0'(4(3(2(3(1(z0)))))) → c24(0'(0(1(3(4(4(z0)))))), 0'(3(1(z0))))
0'(4(3(2(3(1(z0)))))) → c24(0'(1(3(4(4(4(0(z0))))))), 0'(3(1(z0))))
0'(4(3(2(3(1(1(z0))))))) → c24(0'(0(1(4(1(3(4(z0))))))), 0'(3(1(1(z0)))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(z0))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(4(4(z0))))))), 0'(1(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(0(2(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(4(3(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(3(4(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(5(5(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(2(4(4(3(4(0(z0))))))), 0'(3(2(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(1(4(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(4(3(z0))))), 0'(4(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(0(0(3(4(2(1(z0))))))), 0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(1(3(4(0(2(2(z0))))))), 0'(3(2(2(z0)))))
0'(4(3(2(4(1(2(z0))))))) → c24(0'(1(4(0(2(5(z0)))))), 0'(4(1(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(2(3(4(4(0(0(z0))))))), 0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(4(3(5(4(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(5(3(4(0(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(0(2(5(1(3(3(z0))))))), 0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(1(2(z0)))))))) → c24(0'(0(2(4(1(1(5(z0))))))), 0'(5(1(1(2(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c24(0'(0(2(5(2(1(2(z0))))))), 0'(5(1(2(2(z0))))))
0'(4(3(2(5(5(3(2(z0)))))))) → c24(0'(0(2(5(1(3(5(z0))))))), 0'(5(5(3(2(z0))))))

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(z0))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(4(4(z0))))))), 0'(1(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(0(2(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(4(3(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(3(4(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(5(5(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(2(4(4(3(4(0(z0))))))), 0'(3(2(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(1(4(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(4(3(z0))))), 0'(4(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(0(0(3(4(2(1(z0))))))), 0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(1(3(4(0(2(2(z0))))))), 0'(3(2(2(z0)))))
0'(4(3(2(4(1(2(z0))))))) → c24(0'(1(4(0(2(5(z0)))))), 0'(4(1(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(2(3(4(4(0(0(z0))))))), 0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(4(3(5(4(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(5(3(4(0(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(0(2(5(1(3(3(z0))))))), 0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(1(2(z0)))))))) → c24(0'(0(2(4(1(1(5(z0))))))), 0'(5(1(1(2(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c24(0'(0(2(5(2(1(2(z0))))))), 0'(5(1(2(2(z0))))))
0'(4(3(2(5(5(3(2(z0)))))))) → c24(0'(0(2(5(1(3(5(z0))))))), 0'(5(5(3(2(z0))))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c24

(23) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 11 of 34 dangling nodes:

0'(4(3(2(1(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(1(2(z0))))
0'(4(3(2(4(1(2(z0))))))) → c24(0'(1(4(0(2(5(z0)))))), 0'(4(1(2(z0)))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(4(4(z0))))))), 0'(1(2(z0))))
0'(4(3(2(1(2(z0)))))) → c24(0'(0(0(2(1(z0))))), 0'(1(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(4(3(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(2(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(2(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(2(1(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(4(1(z0)))))) → c24(0'(0(1(4(4(z0))))), 0'(4(1(z0))))
0'(4(3(2(5(1(1(2(z0)))))))) → c24(0'(0(2(4(1(1(5(z0))))))), 0'(5(1(1(2(z0))))))
0'(4(3(2(5(5(3(2(z0)))))))) → c24(0'(0(2(5(1(3(5(z0))))))), 0'(5(5(3(2(z0))))))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(0(2(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(4(3(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(3(4(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(5(5(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(2(4(4(3(4(0(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(0(0(3(4(2(1(z0))))))), 0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(1(3(4(0(2(2(z0))))))), 0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(2(3(4(4(0(0(z0))))))), 0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(4(3(5(4(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(5(3(4(0(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(0(2(5(1(3(3(z0))))))), 0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c24(0'(0(2(5(2(1(2(z0))))))), 0'(5(1(2(2(z0))))))

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(0(2(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(4(3(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(3(4(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(5(5(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(2(4(4(3(4(0(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(0(0(3(4(2(1(z0))))))), 0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(1(3(4(0(2(2(z0))))))), 0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(2(3(4(4(0(0(z0))))))), 0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(4(3(5(4(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(5(3(4(0(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(0(2(5(1(3(3(z0))))))), 0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c24(0'(0(2(5(2(1(2(z0))))))), 0'(5(1(2(2(z0))))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c24

(25) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(0(2(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(4(3(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(3(4(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(5(5(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(2(4(4(3(4(0(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(0(0(3(4(2(1(z0))))))), 0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(1(3(4(0(2(2(z0))))))), 0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(2(3(4(4(0(0(z0))))))), 0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(4(3(5(4(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(5(3(4(0(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(0(2(5(1(3(3(z0))))))), 0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(0(2(5(2(1(2(z0))))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(z0))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(0(2(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(4(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(4(3(3(z0)))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(1(3(3(4(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(0(2(3(4(5(5(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(z0)))))) → c24(0'(2(4(4(3(4(0(z0))))))), 0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(0(0(3(4(2(1(z0))))))), 0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(1(3(4(0(2(2(z0))))))), 0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(2(3(4(4(0(0(z0))))))), 0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(4(3(5(4(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(0(1(5(3(4(0(z0))))))), 0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(0(2(5(1(3(3(z0))))))), 0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(0(2(5(2(1(2(z0))))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c24, c1

(27) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 15 trailing tuple parts

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c1, c24, c1

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(3(2(2(z0)))) → c(2'(z0))

We considered the (Usable) Rules:none
And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = [4]   
POL(1(x₁)) = 0   
POL(2(x₁)) = 0   
POL(2'(x₁)) = [3]   
POL(3(x₁)) = 0   
POL(4(x₁)) = 0   
POL(5(x₁)) = 0   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c1, c24, c1

(31) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(4(3(2(5(1(2(2(z0)))))))) → c1

We considered the (Usable) Rules:none
And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = [1]   
POL(1(x₁)) = [5]   
POL(2(x₁)) = [3]   
POL(2'(x₁)) = 0   
POL(3(x₁)) = [3]   
POL(4(x₁)) = [5]   
POL(5(x₁)) = [3]   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c1, c24, c1

(33) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(3(1(z0))) → c3(0'(z0))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))

We considered the (Usable) Rules:none
And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = [4]x₁   
POL(1(x₁)) = [1] + x₁   
POL(2(x₁)) = [2]x₁   
POL(2'(x₁)) = 0   
POL(3(x₁)) = x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1
0'(3(1(z0))) → c3(0'(z0))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c1, c24, c1

(35) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

2'(3(1(z0))) → c40(2'(z0))

We considered the (Usable) Rules:none
And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = [4] + [2]x₁   
POL(1(x₁)) = [2] + x₁   
POL(2(x₁)) = x₁   
POL(2'(x₁)) = [3] + x₁   
POL(3(x₁)) = x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

S tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1
0'(3(1(z0))) → c3(0'(z0))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
2'(3(1(z0))) → c40(2'(z0))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c1, c24, c1

(37) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(3(1(z0))) → c5(0'(z0))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))

We considered the (Usable) Rules:none
And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = [2]x₁   
POL(1(x₁)) = [1] + x₁   
POL(2(x₁)) = [2]x₁   
POL(2'(x₁)) = 0   
POL(3(x₁)) = x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

S tuples:

2'(3(1(z0))) → c38(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1
0'(3(1(z0))) → c3(0'(z0))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c5(0'(z0))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c1, c24, c1

(39) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))

We considered the (Usable) Rules:none
And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = [2]x₁   
POL(2'(x₁)) = 0   
POL(3(x₁)) = [2] + x₁   
POL(4(x₁)) = x₁   
POL(5(x₁)) = x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

S tuples:

2'(3(1(z0))) → c38(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1
0'(3(1(z0))) → c3(0'(z0))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c5(0'(z0))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c1, c24, c1

(41) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))

We considered the (Usable) Rules:none
And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = [3] + [2]x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = [4]x₁   
POL(2'(x₁)) = [3]   
POL(3(x₁)) = x₁   
POL(4(x₁)) = [1] + x₁   
POL(5(x₁)) = x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

S tuples:

2'(3(1(z0))) → c38(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1
0'(3(1(z0))) → c3(0'(z0))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c5(0'(z0))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c1, c24, c1

(43) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))

We considered the (Usable) Rules:none
And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = [2] + x₁   
POL(1(x₁)) = x₁   
POL(2(x₁)) = [2]x₁   
POL(2'(x₁)) = [1]   
POL(3(x₁)) = x₁   
POL(4(x₁)) = [1] + x₁   
POL(5(x₁)) = x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

S tuples:

2'(3(1(z0))) → c38(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1
0'(3(1(z0))) → c3(0'(z0))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c5(0'(z0))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c1, c24, c1

(45) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

2'(3(1(z0))) → c38(2'(z0))
0'(3(2(z0))) → c13(0'(z0))

We considered the (Usable) Rules:none
And the Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = [4] + [4]x₁   
POL(1(x₁)) = [5] + x₁   
POL(2(x₁)) = [5]x₁   
POL(2'(x₁)) = [3] + [3]x₁   
POL(3(x₁)) = [1] + x₁   
POL(4(x₁)) = [4] + x₁   
POL(5(x₁)) = [5] + x₁   
POL(c(x₁)) = x₁   
POL(c1) = 0   
POL(c1(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c24(x₁)) = x₁   
POL(c26(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c38(x₁)) = x₁   
POL(c40(x₁)) = x₁   
POL(c5(x₁)) = x₁   

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

0(1(2(z0))) → 0(0(2(1(z0))))
0(1(2(z0))) → 0(2(1(3(z0))))
0(1(2(z0))) → 0(0(2(1(4(4(z0))))))
0(3(1(z0))) → 0(1(3(4(0(z0)))))
0(3(1(z0))) → 0(1(3(4(4(z0)))))
0(3(1(z0))) → 1(3(4(4(4(0(z0))))))
0(3(2(z0))) → 0(2(1(3(z0))))
0(3(2(z0))) → 0(2(3(4(z0))))
0(3(2(z0))) → 0(0(2(4(3(z0)))))
0(3(2(z0))) → 0(2(1(4(3(z0)))))
0(3(2(z0))) → 0(2(4(3(3(z0)))))
0(3(2(z0))) → 0(2(1(3(3(4(z0))))))
0(3(2(z0))) → 0(2(3(4(5(5(z0))))))
0(3(2(z0))) → 2(4(4(3(4(0(z0))))))
0(4(1(z0))) → 0(1(4(4(z0))))
0(4(1(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(1(4(z0))))
0(4(2(z0))) → 0(2(3(4(z0))))
0(4(2(z0))) → 0(2(4(3(z0))))
0(2(0(1(z0)))) → 5(0(0(2(1(z0)))))
0(3(1(1(z0)))) → 0(1(4(1(3(4(z0))))))
0(3(2(1(z0)))) → 0(0(3(4(2(1(z0))))))
0(3(2(2(z0)))) → 1(3(4(0(2(2(z0))))))
0(4(1(2(z0)))) → 1(4(0(2(5(z0)))))
0(4(3(2(z0)))) → 2(3(4(4(0(0(z0))))))
0(5(3(1(z0)))) → 0(1(4(3(5(4(z0))))))
0(5(3(1(z0)))) → 0(1(5(3(4(0(z0))))))
0(5(3(2(z0)))) → 0(2(4(5(3(z0)))))
0(5(3(2(z0)))) → 0(2(5(3(3(z0)))))
0(0(3(2(1(z0))))) → 0(0(1(3(5(2(z0))))))
0(1(0(3(2(z0))))) → 0(1(4(3(2(0(z0))))))
0(1(0(3(2(z0))))) → 2(3(1(0(0(5(z0))))))
0(3(2(5(1(z0))))) → 0(2(5(1(3(3(z0))))))
0(5(1(1(2(z0))))) → 0(2(4(1(1(5(z0))))))
0(5(1(2(2(z0))))) → 0(2(5(2(1(2(z0))))))
0(5(3(2(1(z0))))) → 0(1(3(4(2(5(z0))))))
0(5(5(3(2(z0))))) → 0(2(5(1(3(5(z0))))))
2(0(1(z0))) → 5(0(2(1(z0))))
2(3(1(z0))) → 1(3(5(2(z0))))
2(3(1(z0))) → 0(2(1(3(5(z0)))))
2(3(1(z0))) → 1(4(3(5(2(z0)))))
2(0(3(1(z0)))) → 2(0(1(3(5(2(z0))))))
2(0(4(1(z0)))) → 2(0(1(4(5(z0)))))
2(5(3(2(z0)))) → 2(5(2(3(3(z0)))))
2(5(4(2(z0)))) → 0(2(5(2(4(z0)))))
2(0(3(1(1(z0))))) → 2(1(0(1(3(4(z0))))))
2(2(0(3(1(z0))))) → 1(3(0(2(5(2(z0))))))
2(2(0(5(1(z0))))) → 2(0(2(1(5(1(z0))))))
2(5(5(4(1(z0))))) → 5(5(2(1(3(4(z0))))))

Tuples:

0'(3(1(z0))) → c5(0'(z0))
2'(3(1(z0))) → c38(2'(z0))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c3(0'(z0))
0'(5(3(1(z0)))) → c26(0'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(z0))) → c13(0'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(5(1(2(2(z0)))))))) → c1

S tuples:

0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))

K tuples:

0'(5(3(1(z0)))) → c26(0'(z0))
0'(5(1(2(2(z0))))) → c(2'(z0))
0'(3(2(2(z0)))) → c(2'(z0))
0'(4(3(2(5(1(2(2(z0)))))))) → c1
0'(3(1(z0))) → c3(0'(z0))
0'(4(3(2(3(2(1(z0))))))) → c24(0'(3(2(1(z0)))))
2'(3(1(z0))) → c40(2'(z0))
0'(3(1(z0))) → c5(0'(z0))
0'(4(3(2(5(3(1(z0))))))) → c24(0'(5(3(1(z0)))))
0'(4(3(2(3(2(5(1(z0)))))))) → c24(0'(3(2(5(1(z0))))))
0'(4(3(2(4(3(2(z0))))))) → c24(0'(4(3(2(z0)))))
0'(4(3(2(3(2(2(z0))))))) → c24(0'(3(2(2(z0)))))
0'(4(3(2(3(2(z0)))))) → c24(0'(3(2(z0))))
2'(3(1(z0))) → c38(2'(z0))
0'(3(2(z0))) → c13(0'(z0))

Defined Rule Symbols:

0, 2

Defined Pair Symbols:

0', 2'

Compound Symbols:

c5, c38, c40, c3, c26, c, c13, c1, c24, c1

(47) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

0'(4(3(2(5(1(2(2(z0)))))))) → c1(0'(5(1(2(2(z0))))))
0'(5(1(2(2(z0))))) → c(2'(z0))

Now S is empty

(48) BOUNDS(O(1), O(1))